| Definitions |  x:A. B(x),  , RandomVariable(p;n), x(s), P   Q, {i..j }, P & Q, t  T,  , Top, S  T, i  j < k,   x. t(x), if b then t else f fi , tt, ff,  A, t ...$L, rv-partial-sum(n;i.X(i)), rv-const(a), A B, False,  T, True, P  Q, P Q, r * s, (i = j), r < s, r + s, a < b, a <p b,  b, a < b, p  q, x f y, , t.2, goset, gset, , t.1, < +>, q_le(r;s), p  q, qpositive(r), r - s, i <z j, b, qeq(r;s), (x.F(x)) o X, r s, q*X, X Y, a b, A c B, SQType(T), {T}, Outcome,  , (X(n)   as n),  x:A. B(x), P Q, suptype(S; T), a  b,   , a  b T , (r/s),  a j < b. E(j), (r) i k < j. E(k), <+*>,  lb i < ub. E(i), r+gp, (op,id) lb i < ub. E(i), *, e, +r, 0, Y, 1/r, FinProbSpace,  , Unit, Dec(P), SqStable(P),  |
| Lemmas | slln-lemma2, nat wf, int seg wf, rv-disjoint wf, length wf nat, top wf, rationals wf, le wf, random-variable wf, subtype rel function, expectation wf, int inc rationals, rv-compose wf, qmul wf, finite-prob-space wf, rv-partial-sum wf, eq int wf, bool wf, iff transitivity, assert wf, eqtt to assert, assert of eq int, rv-const wf, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, rv-scale wf, qdiv wf, int-rational, int-eq-in-rationals, qle wf, squash wf, true wf, p-outcome wf, qsum wf, sum unroll base q, expectation-rv-const, qless wf, qadd wf, qadd preserves qless, qadd comm q, qadd ac 1 q, qinverse q, mon ident q, rv-partial-sum-monotone, q-square-non-neg, bounded-expectation, qless transitivity 1 qorder, decidable int equal, qle weakening eq qorder, rv-le wf, int nzero-rational, nat plus inc int nzero, false wf, nullset-monotone, rv-unbounded wf, qabs wf, q-not-limit-zero-diverges-2, qmul-positive, qmul preserves qle, qless transitivity 2 qorder, qmul comm qrng, qle transitivity qorder, prod sum l q, qsum-non-neg2, qle functionality wrt implies, nat plus wf, sq stable from decidable, decidable qle, qabs-squared, sum split q, qadd preserves qle, qadd inv assoc q, nequal wf, nat plus inc, sum unroll lo q, qadd ident |
